1. Technical Field
The present invention relates to software verification and debugging and more particularly to systems and methods for accelerating model checking by providing synchronous execution constraints.
2. Description of the Related Art
The development of effective techniques for debugging multi-threaded software is widely recognized to be a problem of fundamental practical importance. It is, however, also an extremely challenging one. A key reason for this is that subtle interactions between threads makes multi-threaded software behaviorally complex and hard to analyze, thus necessitating the use of formal methodologies for the analysis. It is not surprising then that the use of model checking—both symbolic and explicit state—for the verification of concurrent software has, for some time, been an active area of research.
Explicit state model checkers, such as Verisoft™ rely on exploring an enumeration of the states and transitions of the concurrent program at hand. Additional techniques such as state hashing for compaction of state representations, and partial order methods are typically used to avoid exploring all interleavings of transitions of the constituent threads. Symbolic model checkers, on the other hand, avoid an explicit enumeration of the state space by using symbolic representations of sets of states and transitions.
One of the first successful approaches in this regard was the use of BDDs to succinctly represent large state spaces for the purpose of model checking. More recently, SAT-based techniques have become popular both for finding bugs using SAT-based Bounded Model Checking (BMC) and for generating proofs via SAT-based Unbounded Model Checking (UMC).
SAT-based techniques strongly rely on search heuristics in order to prune state spaces. A lot of these heuristics depend on leveraging structural information about the system at hand. As a result SAT-based BMC has been shown to be very effective for debugging hardware designs which have a lot of inherent organization that these heuristics exploit. Since software programs are much less structured than hardware circuits developing similar heuristics has proven to be a more difficult problem.